(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(assert (not (=> (and (>= (/ b i) 0) (>= j g 0 e 0)) (>= 0 h))))
(assert (= a (* m o) (mod (to_int a) (to_int m)) o (/ b i)))
(assert (= i (/ b f)))
(assert (= c 0))
(assert (= n (/ c k)))
(assert (= k (/ c n)))
(assert (= d (- g l)))
(assert (= g (/ d l)))
(assert (= l (/ d g)))
(check-sat)
